Report for code.c

Generated on 2025-05-12 21:22:39 by CPAchecker 4.0 / default

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
#include <stdlib.h>  
2
#include <stdio.h>  
3
#include <assert.h>  
4
  
5
#define LEN 10  
6
  
7
extern unsigned __VERIFIER_nondet_uint();  
8
extern void __VERIFIER_assume(int);  
9
  
10
/* EXPLANATION  
11
 * The bug in this code is on line 20,the while loop  
12
 * The line needs to be (low <= high), so that the middle value isn't   
13
 * skipped when low and high converge  
14
 */  
15
  
16
// Preconditions:   
17
// arr is a sorted array  
18
// size is the size of the array arr   
19
int binary_search_function(int arr[], int size, int target) {  
20
  int low = 0;  
21
  int high = size - 1;  
22
  int mid;  
23
  while (low <= high) {  
24
      mid = (low + high)/2;  
25
      if (arr[mid] == target) {  
26
          return mid;  
27
      }  
28
      if (arr[mid] < target) {  
29
          low = mid + 1;  
30
      }  
31
      if (arr[mid] > target) {  
32
          high = mid - 1;  
33
      }  
34
  }  
35
  return -1;  
36
}  
37
  
38
int dumb_sort(int arr[], int len, int target) {  
39
	for (int i=0; i<len; ++i) {  
40
		if (target == arr[i]) {  
41
			return i;  
42
		}  
43
	}  
44
  
45
	return -1;  
46
}  
47
  
48
int main() {  
49
  int arr[LEN] = {   
50
		__VERIFIER_nondet_int(),   
51
		__VERIFIER_nondet_int(),  
52
		__VERIFIER_nondet_int(),  
53
		__VERIFIER_nondet_int(),  
54
    __VERIFIER_nondet_int(),  
55
    __VERIFIER_nondet_int(),  
56
    __VERIFIER_nondet_int(),  
57
    __VERIFIER_nondet_int(),  
58
    __VERIFIER_nondet_int(),  
59
    __VERIFIER_nondet_int(),  
60
  };  
61
  
62
  int x = __VERIFIER_nondet_int();  
63
  
64
	for (int i=0; i<LEN-1; ++i) {  
65
		__VERIFIER_assume(arr[i] < arr[i+1]);  
66
	}  
67
  
68
  int result = binary_search_function(arr, LEN, x);  
69
  printf("Result of binary search is = %d\n", result);  
70
  
71
  // is the result correct? How can you check?  
72
	if (result != dumb_sort(arr, LEN, x)) {  
73
		assert(0);  
74
	}  
75
  
76
  return 1;  
77
}  
1
#include <stdlib.h>  
2
#include <stdio.h>  
3
#include <assert.h>  
4
  
5
#define LEN 10  
6
  
7
extern unsigned __VERIFIER_nondet_uint();  
8
extern void __VERIFIER_assume(int);  
9
  
10
/* EXPLANATION  
11
 * The bug in this code is on line 20,the while loop  
12
 * The line needs to be (low <= high), so that the middle value isn't   
13
 * skipped when low and high converge  
14
 */  
15
  
16
// Preconditions:   
17
// arr is a sorted array  
18
// size is the size of the array arr   
19
int binary_search_function(int arr[], int size, int target) {  
20
  int low = 0;  
21
  int high = size - 1;  
22
  int mid;  
23
  while (low <= high) {  
24
      mid = (low + high)/2;  
25
      if (arr[mid] == target) {  
26
          return mid;  
27
      }  
28
      if (arr[mid] < target) {  
29
          low = mid + 1;  
30
      }  
31
      if (arr[mid] > target) {  
32
          high = mid - 1;  
33
      }  
34
  }  
35
  return -1;  
36
}  
37
  
38
int dumb_sort(int arr[], int len, int target) {  
39
	for (int i=0; i<len; ++i) {  
40
		if (target == arr[i]) {  
41
			return i;  
42
		}  
43
	}  
44
  
45
	return -1;  
46
}  
47
  
48
int main() {  
49
  int arr[LEN] = {   
50
		__VERIFIER_nondet_int(),   
51
		__VERIFIER_nondet_int(),  
52
		__VERIFIER_nondet_int(),  
53
		__VERIFIER_nondet_int(),  
54
    __VERIFIER_nondet_int(),  
55
    __VERIFIER_nondet_int(),  
56
    __VERIFIER_nondet_int(),  
57
    __VERIFIER_nondet_int(),  
58
    __VERIFIER_nondet_int(),  
59
    __VERIFIER_nondet_int(),  
60
  };  
61
  
62
  int x = __VERIFIER_nondet_int();  
63
  
64
	for (int i=0; i<LEN-1; ++i) {  
65
		__VERIFIER_assume(arr[i] < arr[i+1]);  
66
	}  
67
  
68
  int result = binary_search_function(arr, LEN, x);  
69
  printf("Result of binary search is = %d\n", result);  
70
  
71
  // is the result correct? How can you check?  
72
	if (result != dumb_sort(arr, LEN, x)) {  
73
		assert(0);  
74
	}  
75
  
76
  return 1;  
77
}  
1
/* Macros and inline functions to swap the order of bytes in integer values.  
2
   Copyright (C) 1997-2020 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _BYTESWAP_H && !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/byteswap.h> directly; include <byteswap.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_BYTESWAP_H  
24
#define _BITS_BYTESWAP_H 1  
25
  
26
#include <features.h>  
27
#include <bits/types.h>  
28
  
29
/* Swap bytes in 16-bit value.  */  
30
#define __bswap_constant_16(x)					\  
31
  ((__uint16_t) ((((x) >> 8) & 0xff) | (((x) & 0xff) << 8)))  
32
  
33
static __inline __uint16_t  
34
__bswap_16 (__uint16_t __bsx)  
35
{  
36
#if __GNUC_PREREQ (4, 8)  
37
  return __builtin_bswap16 (__bsx);  
38
#else  
39
  return __bswap_constant_16 (__bsx);  
40
#endif  
41
}  
42
  
43
/* Swap bytes in 32-bit value.  */  
44
#define __bswap_constant_32(x)					\  
45
  ((((x) & 0xff000000u) >> 24) | (((x) & 0x00ff0000u) >> 8)	\  
46
   | (((x) & 0x0000ff00u) << 8) | (((x) & 0x000000ffu) << 24))  
47
  
48
static __inline __uint32_t  
49
__bswap_32 (__uint32_t __bsx)  
50
{  
51
#if __GNUC_PREREQ (4, 3)  
52
  return __builtin_bswap32 (__bsx);  
53
#else  
54
  return __bswap_constant_32 (__bsx);  
55
#endif  
56
}  
57
  
58
/* Swap bytes in 64-bit value.  */  
59
#define __bswap_constant_64(x)			\  
60
  ((((x) & 0xff00000000000000ull) >> 56)	\  
61
   | (((x) & 0x00ff000000000000ull) >> 40)	\  
62
   | (((x) & 0x0000ff0000000000ull) >> 24)	\  
63
   | (((x) & 0x000000ff00000000ull) >> 8)	\  
64
   | (((x) & 0x00000000ff000000ull) << 8)	\  
65
   | (((x) & 0x0000000000ff0000ull) << 24)	\  
66
   | (((x) & 0x000000000000ff00ull) << 40)	\  
67
   | (((x) & 0x00000000000000ffull) << 56))  
68
  
69
__extension__ static __inline __uint64_t  
70
__bswap_64 (__uint64_t __bsx)  
71
{  
72
#if __GNUC_PREREQ (4, 3)  
73
  return __builtin_bswap64 (__bsx);  
74
#else  
75
  return __bswap_constant_64 (__bsx);  
76
#endif  
77
}  
78
  
79
#endif /* _BITS_BYTESWAP_H */  
1
/* Inline functions to return unsigned integer values unchanged.  
2
   Copyright (C) 2017-2020 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/uintn-identity.h> directly; include <netinet/in.h> or <endian.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_UINTN_IDENTITY_H  
24
#define _BITS_UINTN_IDENTITY_H 1  
25
  
26
#include <bits/types.h>  
27
  
28
/* These inline functions are to ensure the appropriate type  
29
   conversions and associated diagnostics from macros that convert to  
30
   a given endianness.  */  
31
  
32
static __inline __uint16_t  
33
__uint16_identity (__uint16_t __x)  
34
{  
35
  return __x;  
36
}  
37
  
38
static __inline __uint32_t  
39
__uint32_identity (__uint32_t __x)  
40
{  
41
  return __x;  
42
}  
43
  
44
static __inline __uint64_t  
45
__uint64_identity (__uint64_t __x)  
46
{  
47
  return __x;  
48
}  
49
  
50
#endif /* _BITS_UINTN_IDENTITY_H.  */  
DateTimeLevelComponentMessage
2025-05-1221:22:15:368INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-05-1221:22:15:454INFOCPAchecker.runCPAchecker 4.0 / default (OpenJDK 64-Bit Server VM 17.0.14) started
2025-05-1221:22:15:477INFOCPAchecker.parseParsing CFA from file(s) "code.c"
2025-05-1221:22:16:770WARNINGCheckBindingVisitor.visitUndefined function __VERIFIER_nondet_int found, first called in line 50
2025-05-1221:22:18:003INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2025-05-1221:22:18:017WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.callstack.unsupportedFunctions
2025-05-1221:22:18:017INFOCPAchecker.runAlgorithmStarting analysis ...
2025-05-1221:22:18:029INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2025-05-1221:22:18:037INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
CoreComponentsFactory.createAlgorithm
Using Restarting Algorithm
2025-05-1221:22:18:049INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.run
Loading analysis 1 from file /cpachecker/config/components/parallel-valueAnalysis.properties ...
2025-05-1221:22:18:070INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 90s
2025-05-1221:22:18:433INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:22:18:631INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
InductionStepCase
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:22:18:658INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.run
Starting analysis 1 ...
2025-05-1221:22:18:996INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:19:361INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheckAlgorithm.checkCounterexample
Error path found, starting counterexample check with CPACHECKER.
2025-05-1221:22:19:762WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:22:19:866WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:22:19:878WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:22:19:885WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:22:19:896WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:22:19:902WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:22:19:906WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:22:19:932WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:22:19:950WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:22:19:968WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:22:20:107WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:22:20:225INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:20:292INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:20:531INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheckAlgorithm.checkCounterexample
Error path found, starting counterexample check with CPACHECKER.
2025-05-1221:22:21:544INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:21:790WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsProperties
Cannot map specification // This file is part of CPAchecker,
// a tool for configurable software verification:
// https://cpachecker.sosy-lab.org
//
// SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0
OBSERVER AUTOMATON AssertionAutomaton
// This automaton detects assertions that may fail
// (i.e., a function call to __assert_fail).
INITIAL STATE Init;
STATE USEFIRST Init :
// Match standard calls to __assert_fail with nice message on violations.
MATCH {__assert_fail($1, $2, $3, $4)}
-> ERROR("assertion in $location: Condition $1 failed in $2, line $3");
// Match if assert_fail or assert_func is called with any number of parameters.
MATCH {__assert_fail($?)} || MATCH {__assert_func($?)}
-> ERROR("assertion in $location");
// Print warnings for other common error functions to warn users about potentially wrong specification.
MATCH {assert($?)} && !CHECK(location, "functionName==assert")
-> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking."
GOTO Init;
MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error")
-> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
MATCH {reach_error($?)}
-> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property).
2025-05-1221:22:21:790WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsProperties
Cannot map specification // This file is part of CPAchecker,
// a tool for configurable software verification:
// https://cpachecker.sosy-lab.org
//
// SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0
OBSERVER AUTOMATON AssertionAutomaton
// This automaton detects assertions that may fail
// (i.e., a function call to __assert_fail).
INITIAL STATE Init;
STATE USEFIRST Init :
// Match standard calls to __assert_fail with nice message on violations.
MATCH {__assert_fail($1, $2, $3, $4)}
-> ERROR("assertion in $location: Condition $1 failed in $2, line $3");
// Match if assert_fail or assert_func is called with any number of parameters.
MATCH {__assert_fail($?)} || MATCH {__assert_func($?)}
-> ERROR("assertion in $location");
// Print warnings for other common error functions to warn users about potentially wrong specification.
MATCH {assert($?)} && !CHECK(location, "functionName==assert")
-> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking."
GOTO Init;
MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error")
-> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
MATCH {reach_error($?)}
-> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter."
GOTO Init;
END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property).
2025-05-1221:22:22:275INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:22:22:277INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-05-1221:22:22:284WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
Repository.addMBean
Warning: Error during registration of management interface AbstractionPredicatesMBean (org.sosy_lab.cpachecker:type=predicate,name=AbstractionPredicates)
2025-05-1221:22:22:522WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:22:22:522WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int();
2025-05-1221:22:22:532WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:22:22:532WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int();
2025-05-1221:22:22:540WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:22:22:540WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int();
2025-05-1221:22:22:545WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:22:22:546WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int();
2025-05-1221:22:22:558WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:22:22:558WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int();
2025-05-1221:22:22:568WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:22:22:568WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int();
2025-05-1221:22:22:573WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:22:22:574WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int();
2025-05-1221:22:22:591WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:22:22:593WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int();
2025-05-1221:22:22:593WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:22:22:595WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:22:22:597WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int();
2025-05-1221:22:22:606WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int();
2025-05-1221:22:22:635WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:22:22:635WARNINGAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheck
PredicateCPA
CtoFormulaConverter.getReturnType
line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int();
2025-05-1221:22:22:904INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:23:026INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 1
CounterexampleCheckAlgorithm.checkCounterexample
Error path found but identified as infeasible.
2025-05-1221:22:23:027INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 2
CounterexampleCheckAlgorithm.checkCounterexample
Error path found but identified as infeasible.
2025-05-1221:22:23:051INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 2
2025-05-1221:22:23:052INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:23:066INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:23:067INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:23:159INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:23:527INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:23:614INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 3
2025-05-1221:22:23:614INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:23:619INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:23:620INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:23:679INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:24:179INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:24:320INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 4
2025-05-1221:22:24:321INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:24:328INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:24:328INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:24:395INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:24:907INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:25:157INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 5
2025-05-1221:22:25:158INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:25:176INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:25:177INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:25:220INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:25:841INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:26:200INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 6
2025-05-1221:22:26:201INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:26:205INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:26:205INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:26:244INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:26:754INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:27:108INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 7
2025-05-1221:22:27:109INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:27:116INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:27:116INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:27:159INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:28:051INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:28:472INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 8
2025-05-1221:22:28:473INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:28:476INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:28:478INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:28:586INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:29:321INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:29:787INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 9
2025-05-1221:22:29:788INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:29:791INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:29:791INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:29:823INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:30:665INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:31:326INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 10
2025-05-1221:22:31:326INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:31:422INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:34:285INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:34:906INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Running algorithm to create induction hypothesis
2025-05-1221:22:36:107INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
KInductionProver.check
Starting induction check...
2025-05-1221:22:36:865INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
LoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 11
2025-05-1221:22:36:866INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.run
Creating formula for program
2025-05-1221:22:36:884INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.boundedModelCheck
Starting satisfiability check...
2025-05-1221:22:38:252INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
Parallel analysis 3
AbstractBMCAlgorithm.checkBoundingAssertions
Starting assertions check...
2025-05-1221:22:38:589INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Analysis /cpachecker/config/components/parallel-valueAnalysis.properties
ParallelAlgorithm.handleFutureResults
/cpachecker/config/components/parallel-kInduction.properties finished successfully.
2025-05-1221:22:38:599INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.skipNextAnalysesIfRequired
Ignoring restart configuration '/cpachecker/config/components/recursion.properties' because condition if-recursive did not match.
2025-05-1221:22:38:600INFOAnalysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
RestartAlgorithm.skipNextAnalysesIfRequired
Ignoring restart configuration '/cpachecker/config/components/concurrency.properties' because condition if-concurrent did not match.
2025-05-1221:22:38:600INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set 0
Used algorithm property /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties
Program containing only relevant bools 0
Relevant boolean vars / relevant vars ratio 0.3704
Requires alias handling 0
Requires loop handling 1
Has a single loop 0
Requires composite-type handling 0
Requires array handling 1
Requires float handling 0
Requires recursion handling 0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions true
Number of all righthand side functions 3
Restart Algorithm statistics
Number of algorithms provided 3
Number of algorithms used 3
Last algorithm used /cpachecker/config/components/concurrency.properties
Total time for algorithm 3 20.551s
Parallel Algorithm statistics
Number of algorithms used 3
Successful analysis /cpachecker/config/components/parallel-kInduction.properties
Statistics for /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties
=======================================================================================
Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties 0.002s
ValueAnalysisCPA statistics
Number of variables per state 2.56 sum: 407, count: 159, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 159, min: 0, max: 0
Number of assumptions 84
Number of deterministic assumptions 38
Level of Determinism 45%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 159
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.017s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.084s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 551, count: 551, min: 1, max: 1 [1 x 551]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 145
Max size of waitlist 14
Average size of waitlist 4
Number of computed successors 159
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 0.688s Max: 0.688s
Time for choose from waitlist 0.002s
Time for precision adjustment 0.065s
Time for transfer relation 0.540s
Time for stop operator 0.064s
Time for adding to reached set 0.009s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 3.670s
Statistics for /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties
=======================================================================================
ValueAnalysisCPA statistics
Number of variables per state 1.58 sum: 220, count: 139, min: 0, max: 4
Number of global variables per state 0.00 sum: 0, count: 139, min: 0, max: 0
Number of assumptions 212
Number of deterministic assumptions 50
Level of Determinism 24%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 478
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.049s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.117s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 417
Max size of waitlist 9
Average size of waitlist 2
Number of computed successors 478
Max successors for one state 2
Number of times merged 0
Number of times stopped 50
Number of times breaked 4
Total time for CPA algorithm 0.823s Max: 0.359s
Time for choose from waitlist 0.007s
Time for precision adjustment 0.114s
Time for transfer relation 0.611s
Time for stop operator 0.064s
Time for adding to reached set 0.011s
ValueAnalysisRefiner statistics
Number of refinements 4
Number of targets found 4 count: 4, min: 1, max: 1, avg: 1.00
Time for completing refinement 0.814s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 3
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.062s
Number of interpolations 3
Number of interpolation queries 11 count: 133, min: 0, max: 3, avg: 0.08
Size of interpolant 0.08 sum: 10, count: 133, min: 0, max: 2
Number of sliced prefixes 7 count: 3, min: 1, max: 4, avg: 2.33
Extracting infeasible sliced prefixes 0.210s
Selecting infeasible sliced prefixes 0.017s
CEGAR algorithm statistics
Number of CEGAR refinements 4
Number of successful refinements 3
Number of failed refinements 0
Max. size of reached set before ref. 139
Max. size of reached set after ref. 1
Avg. size of reached set before ref. 108.00
Avg. size of reached set after ref. 1.00
Total time for CEGAR algorithm 1.862s
Time for refinements 1.037s
Average time for refinement 0.259s
Max time for refinement 0.420s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 2.499s
Statistics for /cpachecker/config/components/parallel-kInduction.properties
============================================================================
PredicateCPA statistics
Number of abstractions 120 5% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 0 0%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 120 100%
Times precision was empty 120 100%
Times precision was {false} 0 0%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 0 0%
Times result was 'false' 0 0%
Number of strengthen sat checks 0
Number of coverage checks 64
BDD entailment checks 0
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 170
Avg ABE block size 121.23 sum: 14548, count: 120, min: 72, max: 170
Number of predicates discovered 0
Time for post operator 0.544s
Time for path formula creation 0.529s
Time for strengthen operator 0.055s
Time for prec operator 0.033s
Time for abstraction 0.000s Max: 0.000s, Count: 120
Solving time 0.000s Max: 0.000s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for merge operator 0.003s
Time for coverage checks 0.000s
Total time for SMT solver (w/o itp) 0.000s
Total number of created targets for pointer analysis 0
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
Bounds CPA statistics
Bound k 11
Maximum loop iteration reached 12
ValueAnalysisCPA statistics
Number of variables per state 1.91 sum: 3941, count: 2066, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 2066, min: 0, max: 0
Number of assumptions 830
Number of deterministic assumptions 286
Level of Determinism 34%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 2237
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.008s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.030s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2237, count: 2237, min: 1, max: 1 [1 x 2237]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 2226
Max size of waitlist 190
Average size of waitlist 68
LoopstackSortedWaitlist 3.17 sum: 1692, count: 534, min: 0, max: 707
ReversePostorderSortedWaitlist 2.01 sum: 1102, count: 547, min: 0, max: 698
LoopIterationSortedWaitlist 3.14 sum: 1679, count: 534, min: 0, max: 707
CallstackSortedWaitlist 292.09 sum: 3213, count: 11, min: 2, max: 1692
Number of computed successors 2237
Max successors for one state 2
Number of times merged 32
Number of times stopped 32
Number of times breaked 0
Total time for CPA algorithm 1.372s Max: 1.214s
Time for choose from waitlist 0.080s
Time for precision adjustment 0.173s
Time for transfer relation 0.975s
Time for merge operator 0.011s
Time for stop operator 0.022s
Time for adding to reached set 0.069s
BMC algorithm statistics
Time for BMC formula creation 1.383s
Time for final sat check 4.203s
Time for bounding assertions check 1.272s
Time for induction formula creation 7.462s
Time for induction check 3.613s
Other statistics
================
Parallel Algorithm statistics
Number of algorithms used 3
Successful analysis /cpachecker/config/components/parallel-kInduction.properties
Statistics for /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties
=======================================================================================
Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties 0.002s
ValueAnalysisCPA statistics
Number of variables per state 2.56 sum: 407, count: 159, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 159, min: 0, max: 0
Number of assumptions 84
Number of deterministic assumptions 38
Level of Determinism 45%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 159
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.017s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.084s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 551, count: 551, min: 1, max: 1 [1 x 551]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 145
Max size of waitlist 14
Average size of waitlist 4
Number of computed successors 159
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 0.688s Max: 0.688s
Time for choose from waitlist 0.002s
Time for precision adjustment 0.065s
Time for transfer relation 0.540s
Time for stop operator 0.064s
Time for adding to reached set 0.009s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 3.670s
Statistics for /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties
=======================================================================================
ValueAnalysisCPA statistics
Number of variables per state 1.58 sum: 220, count: 139, min: 0, max: 4
Number of global variables per state 0.00 sum: 0, count: 139, min: 0, max: 0
Number of assumptions 212
Number of deterministic assumptions 50
Level of Determinism 24%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 478
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.049s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.117s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 417
Max size of waitlist 9
Average size of waitlist 2
Number of computed successors 478
Max successors for one state 2
Number of times merged 0
Number of times stopped 50
Number of times breaked 4
Total time for CPA algorithm 0.823s Max: 0.359s
Time for choose from waitlist 0.007s
Time for precision adjustment 0.114s
Time for transfer relation 0.611s
Time for stop operator 0.064s
Time for adding to reached set 0.011s
ValueAnalysisRefiner statistics
Number of refinements 4
Number of targets found 4 count: 4, min: 1, max: 1, avg: 1.00
Time for completing refinement 0.814s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 3
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.062s
Number of interpolations 3
Number of interpolation queries 11 count: 133, min: 0, max: 3, avg: 0.08
Size of interpolant 0.08 sum: 10, count: 133, min: 0, max: 2
Number of sliced prefixes 7 count: 3, min: 1, max: 4, avg: 2.33
Extracting infeasible sliced prefixes 0.210s
Selecting infeasible sliced prefixes 0.017s
CEGAR algorithm statistics
Number of CEGAR refinements 4
Number of successful refinements 3
Number of failed refinements 0
Max. size of reached set before ref. 139
Max. size of reached set after ref. 1
Avg. size of reached set before ref. 108.00
Avg. size of reached set after ref. 1.00
Total time for CEGAR algorithm 1.862s
Time for refinements 1.037s
Average time for refinement 0.259s
Max time for refinement 0.420s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 1 100%
Time for counterexample checks 2.499s
Statistics for /cpachecker/config/components/parallel-kInduction.properties
============================================================================
PredicateCPA statistics
Number of abstractions 120 5% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 0 0%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 120 100%
Times precision was empty 120 100%
Times precision was {false} 0 0%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 0 0%
Times result was 'false' 0 0%
Number of strengthen sat checks 0
Number of coverage checks 64
BDD entailment checks 0
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 170
Avg ABE block size 121.23 sum: 14548, count: 120, min: 72, max: 170
Number of predicates discovered 0
Time for post operator 0.544s
Time for path formula creation 0.529s
Time for strengthen operator 0.055s
Time for prec operator 0.033s
Time for abstraction 0.000s Max: 0.000s, Count: 120
Solving time 0.000s Max: 0.000s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for merge operator 0.003s
Time for coverage checks 0.000s
Total time for SMT solver (w/o itp) 0.000s
Total number of created targets for pointer analysis 0
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
Bounds CPA statistics
Bound k 11
Maximum loop iteration reached 12
ValueAnalysisCPA statistics
Number of variables per state 1.91 sum: 3941, count: 2066, min: 0, max: 5
Number of global variables per state 0.00 sum: 0, count: 2066, min: 0, max: 0
Number of assumptions 830
Number of deterministic assumptions 286
Level of Determinism 34%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 2237
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.008s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (AssertionAutomaton) statistics
Number of states 1
Total time for successor computation 0.030s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2237, count: 2237, min: 1, max: 1 [1 x 2237]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 2226
Max size of waitlist 190
Average size of waitlist 68
LoopstackSortedWaitlist 3.17 sum: 1692, count: 534, min: 0, max: 707
ReversePostorderSortedWaitlist 2.01 sum: 1102, count: 547, min: 0, max: 698
LoopIterationSortedWaitlist 3.14 sum: 1679, count: 534, min: 0, max: 707
CallstackSortedWaitlist 292.09 sum: 3213, count: 11, min: 2, max: 1692
Number of computed successors 2237
Max successors for one state 2
Number of times merged 32
Number of times stopped 32
Number of times breaked 0
Total time for CPA algorithm 1.372s Max: 1.214s
Time for choose from waitlist 0.080s
Time for precision adjustment 0.173s
Time for transfer relation 0.975s
Time for merge operator 0.011s
Time for stop operator 0.022s
Time for adding to reached set 0.069s
BMC algorithm statistics
Time for BMC formula creation 1.383s
Time for final sat check 4.203s
Time for bounding assertions check 1.272s
Time for induction formula creation 7.462s
Time for induction check 3.613s
Other statistics
================
Code Coverage
Function coverage 0.333
Visited lines 466
Total lines 472
Line coverage 0.987
Visited conditions 18
Total conditions 18
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 478
Number of CFA edges (per node) 477 count: 478, min: 0, max: 2, avg: 1.00
Number of relevant variables 27
Number of functions 9
Number of loops (and loop nodes) 3 sum: 18, min: 4, max: 10, avg: 6.00
Size of reached set 2066
Number of reached locations 452 95%
Avg states per location 4
Max states per location 121 at node N50
Number of reached functions 3 33%
Number of target states 0
Time for analysis setup 2.540s
Time for loading CPAs 0.950s
Time for loading parser 0.313s
Time for CFA construction 1.245s
Time for parsing file(s) 0.409s
Time for AST to CFA 0.427s
Time for CFA sanity check 0.039s
Time for post-processing 0.186s
Time for loop structure 0.008s
Time for AST structure 0.000s
Time for CFA export 0.812s
Time for function pointers resolving 0.003s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.105s
Time for collecting variables 0.067s
Time for solving dependencies 0.003s
Time for building hierarchy 0.000s
Time for building classification 0.030s
Time for exporting data 0.005s
Time for Analysis 20.579s
CPU time for analysis 33.150s
Time for analyzing result 0.000s
Total time for CPAchecker 23.128s
Total CPU time for CPAchecker 37.940s
Time for statistics 0.152s
Time for Garbage Collector 0.372s in 63 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 113MB ( 108 MiB) max; 57MB ( 54 MiB) avg; 136MB ( 130 MiB) peak
Used non-heap memory 67MB ( 64 MiB) max; 58MB ( 56 MiB) avg; 69MB ( 65 MiB) peak
Used in PS Old Gen pool 86MB ( 82 MiB) max; 36MB ( 35 MiB) avg; 86MB ( 82 MiB) peak
Allocated heap memory 235MB ( 224 MiB) max; 140MB ( 133 MiB) avg
Allocated non-heap memory 70MB ( 67 MiB) max; 62MB ( 59 MiB) avg
Total process virtual memory 5513MB ( 5257 MiB) max; 5394MB ( 5144 MiB) avg
#Configuration NameConfiguration Value
1analysis.name default
2analysis.programNames code.c
3analysis.selectAnalysisHeuristically true
4cfa.useCFACloningForMultiThreadedPrograms true
5cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp,atexit
6datarace.config dataRaceAnalysis.properties
7heuristicSelection.addressedRatio 0.0
8heuristicSelection.complexLoopConfig components/configselection-restart-valueAnalysis-fallbacks.properties
9heuristicSelection.loopConfig components/multipleLoopsConfig.properties
10heuristicSelection.loopFreeConfig components/configselection-restart-bmc-fallbacks.properties
11heuristicSelection.singleLoopConfig components/singleLoopConfig.properties
12language C
13log.level INFO
14memorycleanup.config smg-memorycleanup.properties
15memorysafety.config smg-memorysafety.properties
16overflow.config overflowAnalysis.properties
17parser.usePreprocessor true
18specification /cpachecker/config/specification/Assertion.spc
19termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}